Nuprl Lemma : member-es-interval 0,22

es:ES, ee'ev:E. (ev  [ee'])  e  ev  & ev  e'  
latex


Definitions{T}, [ee'], P  Q, P  Q, P  Q, filter(P;l), as @ bs, before(e), es-ble{i:l}(es;e;e'), (x  l), b, P & Q, e  e' , Prop, (e <loc e'), P  Q, False, E, x:AB(x), t  T, ES
Lemmasevent system wf, es-E wf, false wf, es-locl wf, l member wf, assert wf, es-le wf, es-ble wf, es-before wf, append wf, filter wf, assert-es-ble, and functionality wrt iff, iff functionality wrt iff, nil member, or functionality wrt iff, cons member, member-es-before, member append, member filter

origin